ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:((?)()()), g:().
combine-ecl-tuples2(A; B; f; g)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions

t  T, x:A. B(x), A  B, P  Q, False, A, , decl-state(ds), ma-valtype(da; k), Unit, , ff, , x. t(x), t.2, t.1, bor(p; q), reduce(f; k; as), Knd, (x  l), b, prop{i:l}, b, P  Q, P  Q, append(as; bs), EqDecider(T), if b then t else f fi , subtype(S; T), combine-halt-info(ea; eb; f; g; x), merge(as; bs), , spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), let x = a in b(x), combine-ecl-tuples2(A; B; f; g), ecl-trans-tuple{i:l}(ds; da), Id, fpf(A; a.B(a)), Kind-deq, deq-member(eq; x; L)

Lemmas

ecl-trans-tuple wf, fpf wf, Id wf, it wf, merge wf, combine-halt-info wf, nat wf, ifthenelse wf, append wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf, reduce wf, bor wf, nat plus inc, pi1 wf, pi2 wf, nat plus wf, bfalse wf, bool wf, unit wf, ma-valtype wf, decl-state wf, le wf